\begin{tabbing}
1. $n$ : $\mathbb{Z}$
\\[0ex]2. 0 $<$ $n$
\\[0ex]3. \=$\forall$$a$, $b$:$\mathbb{N}$.\+
\\[0ex]\{\=$m$:$\mathbb{N}\mid$ \+
\\[0ex]$\forall$$k$:$\mathbb{N}$.
\\[0ex]($a$ = fib($k$))
\\[0ex]$\Rightarrow$ (($k$ $\leq$ 0) $\Rightarrow$ ($b$ = 0))
\\[0ex]$\Rightarrow$ ((0 $<$ $k$) $\Rightarrow$ ($b$ = fib($k$ {-} 1)))
\\[0ex]$\Rightarrow$ ($m$ = fib(($n$ {-} 1)+$k$))\} 
\-\-\\[0ex]4. $a$ : $\mathbb{N}$
\\[0ex]5. $b$ : $\mathbb{N}$
\\[0ex]6. \=$\forall$$b_{1}$:$\mathbb{N}$.\+
\\[0ex]\{\=$m$:$\mathbb{N}\mid$ \+
\\[0ex]$\forall$$k$:$\mathbb{N}$.
\\[0ex]($a$+$b$ = fib($k$))
\\[0ex]$\Rightarrow$ (($k$ $\leq$ 0) $\Rightarrow$ ($b_{1}$ = 0))
\\[0ex]$\Rightarrow$ ((0 $<$ $k$) $\Rightarrow$ ($b_{1}$ = fib($k$ {-} 1)))
\\[0ex]$\Rightarrow$ ($m$ = fib(($n$ {-} 1)+$k$))\} 
\-\-\\[0ex]7. $m$ : $\mathbb{N}$
\\[0ex]8. \=$\forall$$k$:$\mathbb{N}$.\+
\\[0ex]($a$+$b$ = fib($k$))
\\[0ex]$\Rightarrow$ (($k$ $\leq$ 0) $\Rightarrow$ ($a$ = 0))
\\[0ex]$\Rightarrow$ ((0 $<$ $k$) $\Rightarrow$ ($a$ = fib($k$ {-} 1)))
\\[0ex]$\Rightarrow$ ($m$ = fib(($n$ {-} 1)+$k$))
\-\\[0ex]9. $k$ : $\mathbb{N}$
\\[0ex]10. $a$ = fib($k$)
\\[0ex]11. (0 $<$ $k$) $\Rightarrow$ ($b$ = fib($k$ {-} 1))
\\[0ex]12. $k$ = 0
\\[0ex]13. $b$ = 0
\\[0ex]$\vdash$  $a$+0 = fib(0+1)
\end{tabbing}